/*
 * SatSolver.h
 *
 */

#ifndef SATSOLVER_H_
#define SATSOLVER_H_

#include "SatTask.h"
#include "ArrayList.h"

#define GUESSED -2

inline int literalToVar(int var) {
	return var >> 1;
}

inline int negLiteral(int var) {
	return var ^ 1;
}

inline int oldToNew(int var) {
	if (var > 0) {
		return (var - 1) * 2;
	} else {
		return (-var - 1) * 2 + 1;
	}
}

inline int newToOld(int var) {
	if ((var & 1) == 0) {
		return (var >> 1) + 1;
	} else {
		return -((var >> 1) + 1);
	}
}

enum SolverState {
	normal = 0, sat = 1, in_conflict = 2, unsat = 3
};

class SatSolver;

class SatMachine {
public:
	SatSolver *solver;
	int varsNumber;

	int watchedSize;
	int frameSize;
	SolverState state;

	ArrayList<int> frame;
	ArrayList<int> reasons;
	ArrayList<int> varsValues;

	SatMachine(SatSolver *s, int vars) {
		solver = s;
		varsNumber = vars;

		frame.resize(vars);
		frame.fill(-1);
		reasons.resize(vars);
		reasons.fill(-1);
		varsValues.resize(vars);
		varsValues.fill(-1);

		watchedSize = 0;
		frameSize = 0;
		state = normal;
	}

	void drop(int t) {
		while (frameSize > t) {
			--frameSize;
			int lastVar = frame[frameSize];
			varsValues[literalToVar(lastVar)] = -1;
			frame[frameSize] = -1;
		}
		watchedSize = frameSize = t;
		state = normal;
	}

	void setVarValue(int literal, int reason) {
		int variable = literalToVar(literal);

		varsValues[variable] = literal;
		reasons[variable] = reason;
		frame[frameSize++] = literal;
	}

	int rollback() {
		int var = -1;
		while (frameSize > 0) {
			--frameSize;
			int lastLiteral = frame[frameSize];
			varsValues[literalToVar(lastLiteral)] = -1;
			frame[frameSize] = -1;

			if (reasons[literalToVar(lastLiteral)] == -2) {
				var = negLiteral(lastLiteral);
				break;
			}

		}

		if (var == -1) {
			return false;
		}

		watchedSize = frameSize;
		setVarValue(var, -1);
		state = normal;

		return true;
	}

	bool canFork() {
		if (state != normal) {
			return false;
		}
		for (int i = 0; i < frameSize - varsNumber / 10; i++) {
			int var = literalToVar(frame[i]);
			if (reasons[var] == GUESSED) {
				return true;
			}
		}
		return false;
	}

	void makeFork(SatMachine &machine) {
		machine.watchedSize = watchedSize;
		machine.frameSize = frameSize;
		machine.state = state;

		machine.frame.fastCopy(frame);
		machine.reasons.fastCopy(reasons);
		machine.varsValues.fastCopy(varsValues);

		for (int i = 0; i < frameSize; i++) {
			int var = literalToVar(frame[i]);
			if (reasons[var] == GUESSED) {
				reasons[var] = -1;

				while (machine.reasons[var] == GUESSED) {
					machine.rollback();
				}

				return;
			}
		}

		assertexection(false);
	}

	string toString() {
		ostringstream buff;

		buff << "Frame: " << frame.toString() << "\n";
		buff << "Reas : ";
		for (int i = 0; i < frameSize; i++) {
			if (i > 0) {
				buff << "\t";
			}
			buff << reasons[literalToVar(frame[i])];
		}
		buff << "\n";
		buff << "Vars:  ";
		buff << varsValues.toString() << "\n";
		return buff.str();
	}

	void setFreeVar() {
		for (int var = 0; var < varsNumber; var++) {
			if (varsValues[var] == -1) {
				setVarValue(var * 2, GUESSED);
				return;
			}
		}
	}

	void updateClause(int clauseNum);

	void runSolutionLoop();
};

class SatSolver {
public:
	ArrayList<int> clausesData;
	ArrayList<int> watches;
	ArrayList<int> watchesIndex;

	size_t varsNumber;

	vector<int> result;

	vector<SatMachine> satMachines;
	ArrayList<char> varsForCuda;

public:
	SatSolver(const SatTask &task) {
		varsNumber = task.getVariablesNumber();
		watchesIndex.resize(2 * varsNumber + 1);

		fillClauses(task.getClauses());
		fillWatches(clausesData.size());

		for (int i = 0; i < MAX_PROCESSES; i++) {
			satMachines.push_back(SatMachine(this, varsNumber));
			if (i > 0) {
				satMachines[i].state = unsat;
			}
		}
	}

	~SatSolver() {
	}

	void addClause(const ArrayList<int> &clause) {
		for (size_t j = 0; j < clause.size(); j++) {
			int var = clause[j];
			clausesData.push(var);
		}
		clausesData.push(-1);
	}

	void fillWatches(size_t clausesSize) {
		ArrayList<int> vars;
		vars.resize(2 * varsNumber);
		vars.fill(0);

		for (size_t i = 0; i < clausesSize; i++) {
			int var = clausesData[i];
			if (var != -1) {
				vars[var]++;
			}
		}

		int index = 0;

		for (size_t i = 0; i <= 2 * varsNumber; i++) {
			watchesIndex[i] = index;
			if (i < vars.size()) {
				index += vars[i];
			}
		}

		watches.resize(index);

		int last = 0;
		for (size_t i = 0; i < clausesSize; i++) {
			int var = clausesData[i];
			if (var == -1) {
				last = i + 1;
			} else {
				index = watchesIndex[var];
				--vars[var];
				watches[index + vars[var]] = last;
			}
		}
	}

	int fillClauses(const vector<Clause>& clauses) {
		for (size_t i = 0; i < clauses.size(); i++) {
			ArrayList<int> tmp;
			const vector<int> &t = clauses[i].getVariables();
			for (size_t i = 0; i < t.size(); i++) {
				tmp.push(oldToNew(t[i]));
			}
			addClause(tmp);
		}
		return 0;
	}

	void init() {
	}

	void doAllForks(vector<int>& freeSolvers) {
		if (freeSolvers.size() > 0) {
			//printf("Do forks\n");
			for (int i = 0; i < MAX_PROCESSES; i++) {
				if (satMachines[i].canFork()) {
					int t = freeSolvers.back();
					// printf("%d->%d\n", i, t);
					satMachines[i].makeFork(satMachines[t]);

					// std::cout << "Frame: " << satMachines[i].frame.toString() << "\n";
					// std::cout << "Frame: " << satMachines[t].frame.toString() << "\n";

					freeSolvers.pop_back();
					if (freeSolvers.size() == 0) {
						break;
					}
				}
			}
		}
	}

	bool runSolutionLoop() {
		int solversNumber;

		do {
			solversNumber = 0;
			vector<int> freeSolvers;

			for (int i = 0; i < MAX_PROCESSES; i++) {
				SatMachine &satMachine = satMachines[i];
				if ((satMachine.state & 1) == 0) {

					satMachine.runSolutionLoop();

					if (satMachine.state == sat) {
						for (size_t j = 0; j < varsNumber; j++) {
							result.push_back(newToOld(satMachine.varsValues[j]));
						}
						return true;
					}
					solversNumber++;
				} else {
					freeSolvers.push_back(i);
				}
			}
			doAllForks(freeSolvers);
		} while (solversNumber > 0);
		return false;
	}

	vector<int> getVariables() {
		return result;
	}

	void printClause(int clause) {
		printf("(");
		for (int i = clause; clausesData[i] != -1; i++) {
			printf("%d ", newToOld(clausesData[i]));
		}
		printf(")");
	}

};

void SatMachine::updateClause(int clauseNum) {
	int unit = -1;

	for (int i = clauseNum; solver->clausesData[i] != -1; i++) {
		int var = solver->clausesData[i];
		int value = varsValues[literalToVar(var)];
		if (value == var) {
			return;
		}
		if (value == -1) {
			if (unit != -1) {
				return;
			} else {
				unit = var;
			}
		}
	}
	if (unit == -1) {
		state = in_conflict;
	} else {
		setVarValue(unit, clauseNum);
	}
}

void SatMachine::runSolutionLoop() {
	if ((state & 1) == 1) {
		return;
	}

	if (watchedSize == frameSize) {
		setFreeVar();
	}

	int varIndex = negLiteral(frame[watchedSize++]);
	int indexSize = solver->watchesIndex[varIndex + 1];

	for (int i = solver->watchesIndex[varIndex]; i < indexSize; i += 1) {
		updateClause(solver->watches[i]);
		if (state == in_conflict) {
			break;
		}
	}

	if (state == in_conflict) {
		if (!rollback()) {
			state = unsat;
			return;
		}
	}

	if (watchedSize == varsNumber) {
		state = sat;
	}
}

#endif /* SATSOLVER_H_ */
